(declare-fun v () String)
(declare-fun a () Int)
(push)
(assert (and (= 0 (mod 0 a)) (not (str.in_re v (re.* (re.comp (str.to_re "")))))))
(check-sat)
